es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C.
(ff.C r Id)
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 [e: sndr p rcvr]
 (loc(e) = sndr  Id) 

latex

Definitions	x:A. B(x), , P  Q, t  T, [e: i p j], P & Q
Lemmas	snd-it wf, fifoC wf, es-E wf, fifoS wf, Id wf, es-loc wf, FIFO wf, event system wf